proddeq($a$;$b$)($p$,$q$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$1of($a$)(1of($p$),1of($q$)) $\wedge_{2}$ 1of($b$)(2of($p$),2of($q$))